w\_locle($w$;$x$;$y$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$x$ (($\lambda$$x$,$y$. $\neg$first($y$) \& $x$ $=$ pred($y$))$^{\mbox{\scriptsize $\ast$}}$) $y$